Inference at * 1 
Iof proof for Lemma fincr wf2:



  {f | i:  if (i = 0) then  else {f(i - 1)...} fi }  Type 

latex

 by With i,j. i < j MemCD 

latex

 1: .....subterm..... T:t1:n

 1:     Type
 2: .....subterm..... T:t2:n

 2:   (i,j. i < j)  Type
 3: .....eq aux..... NILNIL

 3:   WellFnd{1}(;u,v.(i,j. i < j)(u,v))
 4: .....eq aux..... NILNIL

 4: 1. i : 
 4: 2. f : {f | i:{z:| z (i,j. i < j) i}   if (i = 0) then  else {f(i - 1)...} fi }
 4:   if (i = 0) then  else {f(i - 1)...} fi   Type
 .

Definitions	t  T
Lemmas	int upper wf, ifthenelse wf, nat wf